Add Erdős Problem 1175 (triangle-free subgraph of uncountable chromatic graph)#3786
Add Erdős Problem 1175 (triangle-free subgraph of uncountable chromatic graph)#3786henrykmichalewski wants to merge 5 commits into
Conversation
…atic graph Formalises Problem 1175 asking whether every graph of uncountable chromatic number has a triangle-free subgraph of uncountable chromatic number. Uses chromaticCardinal from upstream, and records Shelah's consistency result for the negative direction when κ=λ=ℵ₁ together with a threshold reformulation. Reference: https://www.erdosproblems.com/1175 Assisted by Claude (Anthropic).
|
Closes #1998 |
Mirrors the Round C docstring pass from the private repo's phase1-infrastructure branch. Each Lean file now carries the canonical source statement and upstream URL inline so reviewers can verify formalization against the source without navigating away from the diff.
| ∀ (κ : Cardinal), ℵ₀ < κ → | ||
| ∃ (μ : Cardinal), | ||
| ∀ (V : Type*) (G : SimpleGraph V), G.chromaticCardinal = μ → | ||
| ∃ (H : G.Subgraph), H.coe.CliqueFree 3 ∧ κ ≤ H.coe.chromaticCardinal := by |
There was a problem hiding this comment.
Does the source ask for a triangle-free subgraph with chromatic number exactly κ? This conclusion only requires κ ≤ H.coe.chromaticCardinal, which is a weaker/different formulation unless there is a reason to use at least. Could you either use equality or add a note explaining why the ≥ κ version is intended?
| wrapping as a `sorry`. | ||
| -/ | ||
| @[category research solved, AMS 5] | ||
| theorem erdos_1175.variants.shelah_consistency : |
There was a problem hiding this comment.
Should this consistency result be stated as an outright negation in the ambient theory? The prose says Shelah proved consistency of a counterexample, not that ZFC proves this negation. Could you encode the extra model-theoretic or axiom hypothesis explicitly, or keep this as a documented consistency placeholder rather than a bare negation?
Paul-Lez
added
the
awaiting-author
…consistency placeholder (Paul-Lez review) Two fixes per Paul-Lez's review: - The headline used `κ ≤ H.coe.chromaticCardinal`, but the source asks for a triangle-free subgraph with chromatic number EXACTLY κ. Changed to `H.coe.chromaticCardinal = κ` in the headline and in the threshold variant (and the supporting `threshold_implies_exact`). - The Shelah consistency variant was stated as a bare ZFC negation. Wrapped it as `answer(sorry)` and documented that this is a consistency placeholder requiring an extra-axiom or model-theoretic encoding outside ZFC.
|
Thanks for the review @PaulLez. Pushed d305709 on |
mo271
left a comment
mo271
left a comment
There was a problem hiding this comment.
Good formalization with correct math and nice Mathlib API usage! A few issues:
- Problem statement duplicated 4 times
The problem text appears at line 23 (verbatim quote), lines 34–36 ("Problem statement" section), lines 61–63 (erdos_1175 docstring), and paraphrased again at lines 106–109 (threshold_formulation docstring). Per project conventions, the problem should appear only once — keep the verbatim quote and remove the redundant copies. The variant docstrings should describe how they differ from the main statement, not restate it.
- Non-standard module docstring formatting
The module docstring uses non-standard headers: Verbatim statement (Erdős #1175, status O):, Source:, Notes: OPEN. These should be replaced with the standard format:
Reference: erdosproblems.com/1175
The "Status", "Formalization notes", etc. sections add useful context but the metadata duplication ("Source", "Notes: OPEN") should be removed.
- threshold_implies_exact naming
erdos_1175.threshold_implies_exact (line 156) is missing a .variants or .test prefix to match the naming pattern of the other declarations (erdos_1175.variants.shelah_consistency, erdos_1175.variants.threshold_formulation). Suggest renaming to erdos_1175.variants.threshold_implies_exact or erdos_1175.test.threshold_implies_exact.
- Redundant test
Test 3 (line 148, (⊥ : SimpleGraph V).CliqueFree 3) is already subsumed by Test 2 (line 142), which uses ⊥ as the witness for ∃ H : G.Subgraph, H.coe.CliqueFree 3. Consider removing the redundant standalone test.
| the ⊥ subgraph witnesses triangle-freeness (though the chromatic number condition is | ||
| what makes the main problem hard). -/ | ||
| @[category test, AMS 5] | ||
| example (V : Type*) (G : SimpleGraph V) : ∃ H : G.Subgraph, H.coe.CliqueFree 3 := |
There was a problem hiding this comment.
instead of using example prefer named theorem names
| @[category test, AMS 5] | ||
| example : ℵ₀ < ℵ_ 1 := by | ||
| rw [← Cardinal.aleph_zero, Cardinal.aleph_lt_aleph] | ||
| exact zero_lt_one |
There was a problem hiding this comment.
| exact zero_lt_one |
No need to explain what example section does.
also the example is not needed: aleph0_lt_aleph_one is already in mathlib
Per PR google-deepmind#3786 review: - Trim module docstring: removed duplicated 'Verbatim statement' / 'Source' / 'Notes' / '## Problem statement' / '## Status' sections; keep only the standard *Reference:* link and the formalization notes. - Trim erdos_1175 docstring: drop redundant '**Note on the answer**' bloat. - Trim erdos_1175.variants.threshold_formulation docstring. - Drop the duplicate aleph0_lt_aleph_one example test (already in Mathlib). - Drop the redundant Test 3 ((⊥ : SimpleGraph V).CliqueFree 3) — subsumed by the triangle-free-subgraph existence test that uses ⊥ as witness. - Promote the two remaining tests from `example` to named theorems erdos_1175.test.exists_triangle_free_subgraph and erdos_1175.test.threshold_implies_exact (the latter renamed from the prefix-less erdos_1175.threshold_implies_exact). Builds cleanly: lake build FormalConjectures.ErdosProblems.«1175»
|
@mo271 — applied all 4 issues + both inline suggestions in
Net diff: -64 / +17. Build green. |
mo271
removed
the
awaiting-author
3 participants
Formalises Erdős Problem 1175: does every graph of uncountable chromatic number contain a triangle-free subgraph of uncountable chromatic number?
Contents
chromaticCardinalfrom upstream.Assisted by Claude (Anthropic).